The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

quicksort(Cons(x, Cons(x', xs))) → part(x, Cons(x', xs))
quicksort(Cons(x, Nil)) → Cons(x, Nil)
quicksort(Nil) → Nil
partLt(x', Cons(x, xs)) → partLt[Ite][True][Ite](<(x, x'), x', Cons(x, xs))
partLt(x, Nil) → Nil
partGt(x', Cons(x, xs)) → partGt[Ite][True][Ite](>(x, x'), x', Cons(x, xs))
partGt(x, Nil) → Nil
app(Cons(x, xs), ys) → Cons(x, app(xs, ys))
app(Nil, ys) → ys
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
part(x, xs) → app(quicksort(partLt(x, xs)), Cons(x, quicksort(partGt(x, xs))))
goal(xs) → quicksort(xs)

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
>(S(x), S(y)) → >(x, y)
>(0, y) → False
>(S(x), 0) → True
partLt[Ite][True][Ite](True, x', Cons(x, xs)) → Cons(x, partLt(x', xs))
partGt[Ite][True][Ite](True, x', Cons(x, xs)) → Cons(x, partGt(x', xs))
partLt[Ite][True][Ite](False, x', Cons(x, xs)) → partLt(x', xs)
partGt[Ite][True][Ite](False, x', Cons(x, xs)) → partGt(x', xs)

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
partLt(S(y39712_1), Cons(0, xs)) →⁺ Cons(0, partLt(S(y39712_1), xs))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [xs / Cons(0, xs)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)